home *** CD-ROM | disk | FTP | other *** search
/ Info-Mac 11 / Info-Mac_XI_Disc_1.cdr_ / Info-Mac XI Disc 1.cdr / Programs / Science & Math / MacEspresso 1.0 / espresso / compl.c < prev    next >
Encoding:
C/C++ Source or Header  |  1989-02-26  |  16.7 KB  |  668 lines  |  [TEXT/R*ch]
  1. /*
  2.  *  module: compl.c
  3.  *  purpose: compute the complement of a multiple-valued function
  4.  *
  5.  *  The "unate recursive paradigm" is used.  After a set of special
  6.  *  cases are examined, the function is split on the "most active
  7.  *  variable".  These two halves are complemented recursively, and then
  8.  *  the results are merged.
  9.  *
  10.  *  Changes (from Version 2.1 to Version 2.2)
  11.  *      1. Minor bug in compl_lifting -- cubes in the left half were
  12.  *      not marked as active, so that when merging a leaf from the left
  13.  *      hand side, the active flags were essentially random.  This led
  14.  *      to minor impredictability problem, but never affected the
  15.  *      accuracy of the results.
  16.  */
  17.  
  18. #include "espresso.h"
  19.  
  20. #define USE_COMPL_LIFT            0
  21. #define USE_COMPL_LIFT_ONSET        1
  22. #define USE_COMPL_LIFT_ONSET_COMPLEX    2
  23. #define NO_LIFTING            3
  24.  
  25. bool compl_special_cases();
  26. pcover compl_merge();
  27. void compl_d1merge();
  28. pcover compl_cube();
  29. void compl_lift();
  30. void compl_lift_onset();
  31. void compl_lift_onset_complex();
  32. bool simp_comp_special_cases();
  33. bool simplify_special_cases();
  34.  
  35.  
  36. /* complement -- compute the complement of T */
  37. pcover complement(T)
  38. pcube *T;            /* T will be disposed of */
  39. {
  40.     register pcube cl, cr;
  41.     register int best;
  42.     pcover Tbar, Tl, Tr;
  43.     int lifting;
  44.     static int compl_level = 0;
  45.  
  46.     if (debug & COMPL)
  47.     debug_print(T, "COMPLEMENT", compl_level++);
  48.  
  49.     if (compl_special_cases(T, &Tbar) == MAYBE) {
  50.  
  51.     /* Allocate space for the partition cubes */
  52.     cl = new_cube();
  53.     cr = new_cube();
  54.     best = binate_split_select(T, cl, cr, COMPL);
  55.  
  56.     /* Complement the left and right halves */
  57.     Tl = complement(scofactor(T, cl, best));
  58.     Tr = complement(scofactor(T, cr, best));
  59.  
  60.     if (Tr->count*Tl->count > (Tr->count+Tl->count)*CUBELISTSIZE(T)) {
  61.         lifting = USE_COMPL_LIFT_ONSET;
  62.     } else {
  63.         lifting = USE_COMPL_LIFT;
  64.     }
  65.     Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
  66.  
  67.     free_cube(cl);
  68.     free_cube(cr);
  69.     free_cubelist(T);
  70.     }
  71.  
  72.     if (debug & COMPL)
  73.     debug1_print(Tbar, "exit COMPLEMENT", --compl_level);
  74.     return Tbar;
  75. }
  76.  
  77. static bool compl_special_cases(T, Tbar)
  78. pcube *T;            /* will be disposed if answer is determined */
  79. pcover *Tbar;            /* returned only if answer determined */
  80. {
  81.     register pcube *T1, p, ceil, cof=T[0];
  82.     pcover A, ceil_compl;
  83.  
  84.     /* Check for no cubes in the cover */
  85.     if (T[2] == NULL) {
  86.     *Tbar = sf_addset(new_cover(1), cube.fullset);
  87.     free_cubelist(T);
  88.     return TRUE;
  89.     }
  90.  
  91.     /* Check for only a single cube in the cover */
  92.     if (T[3] == NULL) {
  93.     *Tbar = compl_cube(set_or(cof, cof, T[2]));
  94.     free_cubelist(T);
  95.     return TRUE;
  96.     }
  97.  
  98.     /* Check for a row of all 1's (implies complement is null) */
  99.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  100.     if (full_row(p, cof)) {
  101.         *Tbar = new_cover(0);
  102.         free_cubelist(T);
  103.         return TRUE;
  104.     }
  105.     }
  106.  
  107.     /* Check for a column of all 0's which can be factored out */
  108.     ceil = set_save(cof);
  109.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  110.     INLINEset_or(ceil, ceil, p);
  111.     }
  112.     if (! setp_equal(ceil, cube.fullset)) {
  113.     ceil_compl = compl_cube(ceil);
  114.     (void) set_or(cof, cof, set_diff(ceil, cube.fullset, ceil));
  115.     set_free(ceil);
  116.     *Tbar = sf_append(complement(T), ceil_compl);
  117.     return TRUE;
  118.     }
  119.     set_free(ceil);
  120.  
  121.     /* Collect column counts, determine unate variables, etc. */
  122.     massive_count(T);
  123.  
  124.     /* If single active variable not factored out above, then tautology ! */
  125.     if (cdata.vars_active == 1) {
  126.     *Tbar = new_cover(0);
  127.     free_cubelist(T);
  128.     return TRUE;
  129.  
  130.     /* Check for unate cover */
  131.     } else if (cdata.vars_unate == cdata.vars_active) {
  132.     A = map_cover_to_unate(T);
  133.     free_cubelist(T);
  134.     A = unate_compl(A);
  135.     *Tbar = map_unate_to_cover(A);
  136.     sf_free(A);
  137.     return TRUE;
  138.  
  139.     /* Not much we can do about it */
  140.     } else {
  141.     return MAYBE;
  142.     }
  143. }
  144.  
  145. /*
  146.  *  compl_merge -- merge the two cofactors around the splitting
  147.  *  variable
  148.  *
  149.  *  The merge operation involves intersecting each cube of the left
  150.  *  cofactor with cl, and intersecting each cube of the right cofactor
  151.  *  with cr.  The union of these two covers is the merged result.
  152.  *
  153.  *  In order to reduce the number of cubes, a distance-1 merge is
  154.  *  performed (note that two cubes can only combine distance-1 in the
  155.  *  splitting variable).  Also, a simple expand is performed in the
  156.  *  splitting variable (simple implies the covering check for the
  157.  *  expansion is not full containment, but single-cube containment).
  158.  */
  159.  
  160. static pcover compl_merge(T1, L, R, cl, cr, var, lifting)
  161. pcube *T1;            /* Original ON-set */
  162. pcover L, R;            /* Complement from each recursion branch */
  163. register pcube cl, cr;        /* cubes used for cofactoring */
  164. int var;            /* splitting variable */
  165. int lifting;            /* whether to perform lifting or not */
  166. {
  167.     register pcube p, last, pt;
  168.     pcover T, Tbar;
  169.     pcube *L1, *R1;
  170.  
  171.     if (debug & COMPL) {
  172.     printf("compl_merge: left %d, right %d\n", L->count, R->count);
  173.     printf("%s (cl)\n%s (cr)\nLeft is\n", pc1(cl), pc2(cr));
  174.     cprint(L);
  175.     printf("Right is\n");
  176.     cprint(R);
  177.     }
  178.  
  179.     /* Intersect each cube with the cofactored cube */
  180.     foreach_set(L, last, p) {
  181.     INLINEset_and(p, p, cl);
  182.     SET(p, ACTIVE);
  183.     }
  184.     foreach_set(R, last, p) {
  185.     INLINEset_and(p, p, cr);
  186.     SET(p, ACTIVE);
  187.     }
  188.  
  189.     /* Sort the arrays for a distance-1 merge */
  190.     (void) set_copy(cube.temp[0], cube.var_mask[var]);
  191.     qsort((char *) (L1 = sf_list(L)), L->count, sizeof(pset), d1_order);
  192.     qsort((char *) (R1 = sf_list(R)), R->count, sizeof(pset), d1_order);
  193.  
  194.     /* Perform distance-1 merge */
  195.     compl_d1merge(L1, R1);
  196.  
  197.     /* Perform lifting */
  198.     switch(lifting) {
  199.     case USE_COMPL_LIFT_ONSET:
  200.         T = cubeunlist(T1);
  201.         compl_lift_onset(L1, T, cr, var);
  202.         compl_lift_onset(R1, T, cl, var);
  203.         free_cover(T);
  204.         break;
  205.     case USE_COMPL_LIFT_ONSET_COMPLEX:
  206.         T = cubeunlist(T1);
  207.         compl_lift_onset_complex(L1, T, var);
  208.         compl_lift_onset_complex(R1, T, var);
  209.         free_cover(T);
  210.         break;
  211.     case USE_COMPL_LIFT:
  212.         compl_lift(L1, R1, cr, var);
  213.         compl_lift(R1, L1, cl, var);
  214.         break;
  215.     case NO_LIFTING:
  216.         break;
  217.     }
  218.     FREE(L1);
  219.     FREE(R1);
  220.  
  221.     /* Re-create the merged cover */
  222.     Tbar = new_cover(L->count + R->count);
  223.     pt = Tbar->data;
  224.     foreach_set(L, last, p) {
  225.     INLINEset_copy(pt, p);
  226.     Tbar->count++;
  227.     pt += Tbar->wsize;
  228.     }
  229.     foreach_active_set(R, last, p) {
  230.     INLINEset_copy(pt, p);
  231.     Tbar->count++;
  232.     pt += Tbar->wsize;
  233.     }
  234.  
  235.     if (debug & COMPL) {
  236.     printf("Result %d\n", Tbar->count);
  237.     if (verbose_debug)
  238.         cprint(Tbar);
  239.     }
  240.  
  241.     free_cover(L);
  242.     free_cover(R);
  243.     return Tbar;
  244. }
  245.  
  246. /*
  247.  *  compl_lift_simple -- expand in the splitting variable using single
  248.  *  cube containment against the other recursion branch to check
  249.  *  validity of the expansion, and expanding all (or none) of the
  250.  *  splitting variable.
  251.  */
  252. static void compl_lift(A1, B1, bcube, var)
  253. pcube *A1, *B1, bcube;
  254. int var;
  255. {
  256.     register pcube a, b, *B2, lift=cube.temp[4], liftor=cube.temp[5];
  257.     pcube mask = cube.var_mask[var];
  258.  
  259.     (void) set_and(liftor, bcube, mask);
  260.  
  261.     /* for each cube in the first array ... */
  262.     for(; (a = *A1++) != NULL; ) {
  263.     if (TESTP(a, ACTIVE)) {
  264.  
  265.         /* create a lift of this cube in the merging coord */
  266.         (void) set_merge(lift, bcube, a, mask);
  267.  
  268.         /* for each cube in the second array */
  269.         for(B2 = B1; (b = *B2++) != NULL; ) {
  270.         INLINEsetp_implies(lift, b, /* when_false => */ continue);
  271.         /* when_true => fall through to next statement */
  272.  
  273.         /* cube of A1 was contained by some cube of B1, so raise */
  274.         INLINEset_or(a, a, liftor);
  275.         break;
  276.         }
  277.     }
  278.     }
  279. }
  280.  
  281.  
  282.  
  283. /*
  284.  *  compl_lift_onset -- expand in the splitting variable using a
  285.  *  distance-1 check against the original on-set; expand all (or
  286.  *  none) of the splitting variable.  Each cube of A1 is expanded
  287.  *  against the original on-set T.
  288.  */
  289. static void compl_lift_onset(A1, T, bcube, var)
  290. pcube *A1;
  291. pcover T;
  292. pcube bcube;
  293. int var;
  294. {
  295.     register pcube a, last, p, lift=cube.temp[4], mask=cube.var_mask[var];
  296.  
  297.     /* for each active cube from one branch of the complement */
  298.     for(; (a = *A1++) != NULL; ) {
  299.     if (TESTP(a, ACTIVE)) {
  300.  
  301.         /* create a lift of this cube in the merging coord */
  302.         INLINEset_and(lift, bcube, mask);    /* isolate parts to raise */
  303.         INLINEset_or(lift, a, lift);    /* raise these parts in a */
  304.  
  305.         /* for each cube in the ON-set, check for intersection */
  306.         foreach_set(T, last, p) {
  307.         if (cdist0(p, lift)) {
  308.             goto nolift;
  309.         }
  310.         }
  311.         INLINEset_copy(a, lift);        /* save the raising */
  312.         SET(a, ACTIVE);
  313. nolift : ;
  314.     }
  315.     }
  316. }
  317.  
  318. /*
  319.  *  compl_lift_complex -- expand in the splitting variable, but expand all
  320.  *  parts which can possibly expand.
  321.  *  T is the original ON-set
  322.  *  A1 is either the left or right cofactor
  323.  */
  324. static void compl_lift_onset_complex(A1, T, var)
  325. pcube *A1;            /* array of pointers to new result */
  326. pcover T;            /* original ON-set */
  327. int var;            /* which variable we split on */
  328. {
  329.     register int dist;
  330.     register pcube last, p, a, xlower;
  331.  
  332.     /* for each cube in the complement */
  333.     xlower = new_cube();
  334.     for(; (a = *A1++) != NULL; ) {
  335.  
  336.     if (TESTP(a, ACTIVE)) {
  337.  
  338.         /* Find which parts of the splitting variable are forced low */
  339.         INLINEset_clear(xlower, cube.size);
  340.         foreach_set(T, last, p) {
  341.         if ((dist = cdist01(p, a)) < 2) {
  342.             if (dist == 0) {
  343.             fatal("compl: ON-set and OFF-set are not orthogonal");
  344.             } else {
  345.             (void) force_lower(xlower, p, a);
  346.             }
  347.         }
  348.         }
  349.  
  350.         (void) set_diff(xlower, cube.var_mask[var], xlower);
  351.         (void) set_or(a, a, xlower);
  352.         free_cube(xlower);
  353.     }
  354.     }
  355. }
  356.  
  357.  
  358.  
  359. /*
  360.  *  compl_d1merge -- distance-1 merge in the splitting variable
  361.  */
  362. static void compl_d1merge(L1, R1)
  363. register pcube *L1, *R1;
  364. {
  365.     register pcube pl, pr;
  366.  
  367.     /* Find equal cubes between the two cofactors */
  368.     for(pl = *L1, pr = *R1; (pl != NULL) && (pr != NULL); )
  369.     switch (d1_order(L1, R1)) {
  370.         case 1:
  371.         pr = *(++R1); break;            /* advance right pointer */
  372.         case -1:
  373.         pl = *(++L1); break;            /* advance left pointer */
  374.         case 0:
  375.         RESET(pr, ACTIVE);
  376.         INLINEset_or(pl, pl, pr);
  377.         pr = *(++R1);
  378.     }
  379. }
  380.  
  381.  
  382.  
  383. /* compl_cube -- return the complement of a single cube (De Morgan's law) */
  384. static pcover compl_cube(p)
  385. register pcube p;
  386. {
  387.     register pcube diff=cube.temp[7], pdest, mask, full=cube.fullset;
  388.     int var;
  389.     pcover R;
  390.  
  391.     /* Allocate worst-case size cover (to avoid checking overflow) */
  392.     R = new_cover(cube.num_vars);
  393.  
  394.     /* Compute bit-wise complement of the cube */
  395.     INLINEset_diff(diff, full, p);
  396.  
  397.     for(var = 0; var < cube.num_vars; var++) {
  398.     mask = cube.var_mask[var];
  399.     /* If the bit-wise complement is not empty in var ... */
  400.     if (! setp_disjoint(diff, mask)) {
  401.         pdest = GETSET(R, R->count++);
  402.         INLINEset_merge(pdest, diff, full, mask);
  403.     }
  404.     }
  405.     return R;
  406. }
  407.  
  408. /* simp_comp -- quick simplification of T */
  409. void simp_comp(T, Tnew, Tbar)
  410. pcube *T;            /* T will be disposed of */
  411. pcover *Tnew;
  412. pcover *Tbar;
  413. {
  414.     register pcube cl, cr;
  415.     register int best;
  416.     pcover Tl, Tr, Tlbar, Trbar;
  417.     int lifting;
  418.     static int simplify_level = 0;
  419.  
  420.     if (debug & COMPL)
  421.     debug_print(T, "SIMPCOMP", simplify_level++);
  422.  
  423.     if (simp_comp_special_cases(T, Tnew, Tbar) == MAYBE) {
  424.  
  425.     /* Allocate space for the partition cubes */
  426.     cl = new_cube();
  427.     cr = new_cube();
  428.     best = binate_split_select(T, cl, cr, COMPL);
  429.  
  430.     /* Complement the left and right halves */
  431.     simp_comp(scofactor(T, cl, best), &Tl, &Tlbar);
  432.     simp_comp(scofactor(T, cr, best), &Tr, &Trbar);
  433.  
  434.     lifting = USE_COMPL_LIFT;
  435.     *Tnew = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
  436.  
  437.     lifting = USE_COMPL_LIFT;
  438.     *Tbar = compl_merge(T, Tlbar, Trbar, cl, cr, best, lifting);
  439.  
  440.     /* All of this work for nothing ? Let's hope not ... */
  441.     if ((*Tnew)->count > CUBELISTSIZE(T)) {
  442.         sf_free(*Tnew);
  443.         *Tnew = cubeunlist(T);
  444.     }
  445.  
  446.     free_cube(cl);
  447.     free_cube(cr);
  448.     free_cubelist(T);
  449.     }
  450.  
  451.     if (debug & COMPL) {
  452.     debug1_print(*Tnew, "exit SIMPCOMP (new)", simplify_level);
  453.     debug1_print(*Tbar, "exit SIMPCOMP (compl)", simplify_level);
  454.     simplify_level--;
  455.     }
  456. }
  457.  
  458. static bool simp_comp_special_cases(T, Tnew, Tbar)
  459. pcube *T;            /* will be disposed if answer is determined */
  460. pcover *Tnew;            /* returned only if answer determined */
  461. pcover *Tbar;            /* returned only if answer determined */
  462. {
  463.     register pcube *T1, p, ceil, cof=T[0];
  464.     pcube last;
  465.     pcover A;
  466.  
  467.     /* Check for no cubes in the cover (function is empty) */
  468.     if (T[2] == NULL) {
  469.     *Tnew = new_cover(1);
  470.     *Tbar = sf_addset(new_cover(1), cube.fullset);
  471.     free_cubelist(T);
  472.     return TRUE;
  473.     }
  474.  
  475.     /* Check for only a single cube in the cover */
  476.     if (T[3] == NULL) {
  477.     (void) set_or(cof, cof, T[2]);
  478.     *Tnew = sf_addset(new_cover(1), cof);
  479.     *Tbar = compl_cube(cof);
  480.     free_cubelist(T);
  481.     return TRUE;
  482.     }
  483.  
  484.     /* Check for a row of all 1's (function is a tautology) */
  485.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  486.     if (full_row(p, cof)) {
  487.         *Tnew = sf_addset(new_cover(1), cube.fullset);
  488.         *Tbar = new_cover(1);
  489.         free_cubelist(T);
  490.         return TRUE;
  491.     }
  492.     }
  493.  
  494.     /* Check for a column of all 0's which can be factored out */
  495.     ceil = set_save(cof);
  496.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  497.     INLINEset_or(ceil, ceil, p);
  498.     }
  499.     if (! setp_equal(ceil, cube.fullset)) {
  500.     p = new_cube();
  501.     (void) set_diff(p, cube.fullset, ceil);
  502.     (void) set_or(cof, cof, p);
  503.     set_free(p);
  504.     simp_comp(T, Tnew, Tbar);
  505.  
  506.     /* Adjust the ON-set */
  507.     A = *Tnew;
  508.     foreach_set(A, last, p) {
  509.         INLINEset_and(p, p, ceil);
  510.     }
  511.  
  512.     /* Compute the new complement */
  513.     *Tbar = sf_append(*Tbar, compl_cube(ceil));
  514.     set_free(ceil);
  515.     return TRUE;
  516.     }
  517.     set_free(ceil);
  518.  
  519.     /* Collect column counts, determine unate variables, etc. */
  520.     massive_count(T);
  521.  
  522.     /* If single active variable not factored out above, then tautology ! */
  523.     if (cdata.vars_active == 1) {
  524.     *Tnew = sf_addset(new_cover(1), cube.fullset);
  525.     *Tbar = new_cover(1);
  526.     free_cubelist(T);
  527.     return TRUE;
  528.  
  529.     /* Check for unate cover */
  530.     } else if (cdata.vars_unate == cdata.vars_active) {
  531.     /* Make the cover minimum by single-cube containment */
  532.     A = cubeunlist(T);
  533.     *Tnew = sf_contain(A);
  534.  
  535.     /* Now form a minimum representation of the complement */
  536.     A = map_cover_to_unate(T);
  537.     A = unate_compl(A);
  538.     *Tbar = map_unate_to_cover(A);
  539.     sf_free(A);
  540.     free_cubelist(T);
  541.     return TRUE;
  542.  
  543.     /* Not much we can do about it */
  544.     } else {
  545.     return MAYBE;
  546.     }
  547. }
  548.  
  549. /* simplify -- quick simplification of T */
  550. pcover simplify(T)
  551. pcube *T;            /* T will be disposed of */
  552. {
  553.     register pcube cl, cr;
  554.     register int best;
  555.     pcover Tbar, Tl, Tr;
  556.     int lifting;
  557.     static int simplify_level = 0;
  558.  
  559.     if (debug & COMPL) {
  560.     debug_print(T, "SIMPLIFY", simplify_level++);
  561.     }
  562.  
  563.     if (simplify_special_cases(T, &Tbar) == MAYBE) {
  564.  
  565.     /* Allocate space for the partition cubes */
  566.     cl = new_cube();
  567.     cr = new_cube();
  568.  
  569.     best = binate_split_select(T, cl, cr, COMPL);
  570.  
  571.     /* Complement the left and right halves */
  572.     Tl = simplify(scofactor(T, cl, best));
  573.     Tr = simplify(scofactor(T, cr, best));
  574.  
  575.     lifting = USE_COMPL_LIFT;
  576.     Tbar = compl_merge(T, Tl, Tr, cl, cr, best, lifting);
  577.  
  578.     /* All of this work for nothing ? Let's hope not ... */
  579.     if (Tbar->count > CUBELISTSIZE(T)) {
  580.         sf_free(Tbar);
  581.         Tbar = cubeunlist(T);
  582.     }
  583.  
  584.     free_cube(cl);
  585.     free_cube(cr);
  586.     free_cubelist(T);
  587.     }
  588.  
  589.     if (debug & COMPL) {
  590.     debug1_print(Tbar, "exit SIMPLIFY", --simplify_level);
  591.     }
  592.     return Tbar;
  593. }
  594.  
  595. static bool simplify_special_cases(T, Tnew)
  596. pcube *T;            /* will be disposed if answer is determined */
  597. pcover *Tnew;            /* returned only if answer determined */
  598. {
  599.     register pcube *T1, p, ceil, cof=T[0];
  600.     pcube last;
  601.     pcover A;
  602.  
  603.     /* Check for no cubes in the cover */
  604.     if (T[2] == NULL) {
  605.     *Tnew = new_cover(0);
  606.     free_cubelist(T);
  607.     return TRUE;
  608.     }
  609.  
  610.     /* Check for only a single cube in the cover */
  611.     if (T[3] == NULL) {
  612.     *Tnew = sf_addset(new_cover(1), set_or(cof, cof, T[2]));
  613.     free_cubelist(T);
  614.     return TRUE;
  615.     }
  616.  
  617.     /* Check for a row of all 1's (implies function is a tautology) */
  618.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  619.     if (full_row(p, cof)) {
  620.         *Tnew = sf_addset(new_cover(1), cube.fullset);
  621.         free_cubelist(T);
  622.         return TRUE;
  623.     }
  624.     }
  625.  
  626.     /* Check for a column of all 0's which can be factored out */
  627.     ceil = set_save(cof);
  628.     for(T1 = T+2; (p = *T1++) != NULL; ) {
  629.     INLINEset_or(ceil, ceil, p);
  630.     }
  631.     if (! setp_equal(ceil, cube.fullset)) {
  632.     p = new_cube();
  633.     (void) set_diff(p, cube.fullset, ceil);
  634.     (void) set_or(cof, cof, p);
  635.     free_cube(p);
  636.  
  637.     A = simplify(T);
  638.     foreach_set(A, last, p) {
  639.         INLINEset_and(p, p, ceil);
  640.     }
  641.     *Tnew = A;
  642.     set_free(ceil);
  643.     return TRUE;
  644.     }
  645.     set_free(ceil);
  646.  
  647.     /* Collect column counts, determine unate variables, etc. */
  648.     massive_count(T);
  649.  
  650.     /* If single active variable not factored out above, then tautology ! */
  651.     if (cdata.vars_active == 1) {
  652.     *Tnew = sf_addset(new_cover(1), cube.fullset);
  653.     free_cubelist(T);
  654.     return TRUE;
  655.  
  656.     /* Check for unate cover */
  657.     } else if (cdata.vars_unate == cdata.vars_active) {
  658.     A = cubeunlist(T);
  659.     *Tnew = sf_contain(A);
  660.     free_cubelist(T);
  661.     return TRUE;
  662.  
  663.     /* Not much we can do about it */
  664.     } else {
  665.     return MAYBE;
  666.     }
  667. }
  668.